/-
Copyright (c) 2018 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzzard,
Amelia Livingston, Yury Kudryashov
-/
module

public import Mathlib.Algebra.Group.Submonoid.Pointwise
public import Mathlib.Algebra.Module.Defs
public import Mathlib.Data.Nat.Cast.Basic

/-!
# Elementwise monoid structure of additive submonoids

These definitions are a cut-down versions of the ones around `Submodule.mul`, as that API is
usually more useful.

`SMul (AddSubmonoid R) (AddSubmonoid A)` is also provided given `DistribSMul R A`,
and when `R = A` it is definitionally equal to the multiplication on `AddSubmonoid R`.

These are all available in the `Pointwise` locale.

Additionally, it provides various degrees of monoid structure:
* `AddSubmonoid.one`
* `AddSubmonoid.mul`
* `AddSubmonoid.mulOneClass`
* `AddSubmonoid.semigroup`
* `AddSubmonoid.monoid`

which is available globally to match the monoid structure implied by `Submodule.idemSemiring`.

## Implementation notes

Many results about multiplication are derived from the corresponding results about scalar
multiplication, but results requiring right distributivity do not have SMul versions,
due to the lack of a suitable typeclass (unless one goes all the way to `Module`).
-/

@[expose] public section

open AddSubmonoid Set
open scoped Pointwise

variable {M R A : Type*}

namespace AddSubmonoid
section AddMonoidWithOne
variable [AddMonoidWithOne R]

/-- If `R` is an additive monoid with one (e.g., a semiring), then `1 : AddSubmonoid R` is the range
of `Nat.cast : ℕ → R`. -/
protected def one : One (AddSubmonoid R) := ⟨AddMonoidHom.mrange (Nat.castAddMonoidHom R)⟩

scoped[Pointwise] attribute [instance] AddSubmonoid.one

lemma one_eq_mrange : (1 : AddSubmonoid R) = AddMonoidHom.mrange (Nat.castAddMonoidHom R) := rfl

lemma natCast_mem_one (n : ℕ) : (n : R) ∈ (1 : AddSubmonoid R) := ⟨_, rfl⟩

@[simp] lemma mem_one {x : R} : x ∈ (1 : AddSubmonoid R) ↔ ∃ n : ℕ, ↑n = x := .rfl

lemma one_eq_closure : (1 : AddSubmonoid R) = closure {1} := by
  rw [closure_singleton_eq, one_eq_mrange]; congr 1; ext; simp

lemma one_eq_closure_one_set : (1 : AddSubmonoid R) = closure 1 := one_eq_closure

end AddMonoidWithOne

section SMul
variable [AddMonoid R] [AddMonoid A] [DistribSMul R A]

/-- For `M : Submonoid R` and `N : AddSubmonoid A`, `M • N` is the additive submonoid
generated by all `m • n` where `m ∈ M` and `n ∈ N`. -/
protected def smul : SMul (AddSubmonoid R) (AddSubmonoid A) where
  smul M N := ⨆ s : M, N.map (DistribSMul.toAddMonoidHom A s.1)

scoped[Pointwise] attribute [instance] AddSubmonoid.smul

variable {M M' : AddSubmonoid R} {N P : AddSubmonoid A} {m : R} {n : A}

lemma smul_mem_smul (hm : m ∈ M) (hn : n ∈ N) : m • n ∈ M • N :=
  (le_iSup _ ⟨m, hm⟩ : _ ≤ M • N) ⟨n, hn, by rfl⟩

lemma smul_le : M • N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m • n ∈ P :=
  ⟨fun H _m hm _n hn => H <| smul_mem_smul hm hn, fun H =>
    iSup_le fun ⟨m, hm⟩ => map_le_iff_le_comap.2 fun n hn => H m hm n hn⟩

@[elab_as_elim]
protected lemma smul_induction_on {C : A → Prop} {a : A} (ha : a ∈ M • N)
    (hm : ∀ m ∈ M, ∀ n ∈ N, C (m • n)) (hadd : ∀ x y, C x → C y → C (x + y)) : C a :=
  (@smul_le _ _ _ _ _ _ _ ⟨⟨setOf C, hadd _ _⟩, by
    simpa only [smul_zero] using hm _ (zero_mem _) _ (zero_mem _)⟩).2 hm ha

@[simp]
lemma addSubmonoid_smul_bot (S : AddSubmonoid R) : S • (⊥ : AddSubmonoid A) = ⊥ :=
  eq_bot_iff.2 <| smul_le.2 fun m _ n hn => by
    rw [AddSubmonoid.mem_bot] at hn ⊢; rw [hn, smul_zero]

lemma smul_le_smul (h : M ≤ M') (hnp : N ≤ P) : M • N ≤ M' • P :=
  smul_le.2 fun _m hm _n hn => smul_mem_smul (h hm) (hnp hn)

lemma smul_le_smul_left (h : M ≤ M') : M • P ≤ M' • P := smul_le_smul h le_rfl
lemma smul_le_smul_right (h : N ≤ P) : M • N ≤ M • P := smul_le_smul le_rfl h

lemma smul_subset_smul : (↑M : Set R) • (↑N : Set A) ⊆ (↑(M • N) : Set A) :=
  smul_subset_iff.2 fun _i hi _j hj ↦ smul_mem_smul hi hj

lemma addSubmonoid_smul_sup : M • (N ⊔ P) = M • N ⊔ M • P :=
  le_antisymm (smul_le.mpr fun m hm np hnp ↦ by
    refine closure_induction (motive := (fun _ ↦ _ • · ∈ _)) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp)
    · rintro x (hx | hx)
      exacts [le_sup_left (a := M • N) (smul_mem_smul hm hx),
        le_sup_right (a := M • N) (smul_mem_smul hm hx)]
    · apply (smul_zero (A := A) m).symm ▸ (M • N ⊔ M • P).zero_mem
    · intro _ _ _ _ h1 h2; rw [smul_add]; exact add_mem h1 h2)
  (sup_le (smul_le_smul_right le_sup_left) <| smul_le_smul_right le_sup_right)

variable {ι : Sort*}

lemma smul_iSup (T : AddSubmonoid R) (S : ι → AddSubmonoid A) : (T • ⨆ i, S i) = ⨆ i, T • S i :=
  le_antisymm (smul_le.mpr fun t ht s hs ↦ iSup_induction _ (motive := (t • · ∈ _)) hs
    (fun i s hs ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs)
    (by simp_rw [smul_zero]; apply zero_mem) fun x y ↦ by simp_rw [smul_add]; apply add_mem)
  (iSup_le fun i ↦ smul_le_smul_right <| le_iSup _ i)

end SMul

section NonUnitalNonAssocSemiring
variable [NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R}

/-- Multiplication of additive submonoids of a semiring R. The additive submonoid `S * T` is the
smallest R-submodule of `R` containing the elements `s * t` for `s ∈ S` and `t ∈ T`. -/
protected def mul : Mul (AddSubmonoid R) := ⟨fun M N => ⨆ s : M, N.map (AddMonoidHom.mul s.1)⟩

scoped[Pointwise] attribute [instance] AddSubmonoid.mul

lemma mul_mem_mul {m n : R} (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N := smul_mem_smul hm hn

lemma mul_le : M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P := smul_le

@[elab_as_elim]
protected lemma mul_induction_on {C : R → Prop} {r : R} (hr : r ∈ M * N)
    (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)) (ha : ∀ x y, C x → C y → C (x + y)) : C r :=
  AddSubmonoid.smul_induction_on hr hm ha

-- need `add_smul` to generalize to `SMul`
lemma closure_mul_closure (S T : Set R) : closure S * closure T = closure (S * T) := by
  apply le_antisymm
  · refine mul_le.2 fun a ha b hb => ?_
    rw [← AddMonoidHom.mulRight_apply, ← AddSubmonoid.mem_comap]
    refine (closure_le.2 fun a' ha' => ?_) ha
    change b ∈ (closure (S * T)).comap (AddMonoidHom.mulLeft a')
    refine (closure_le.2 fun b' hb' => ?_) hb
    change a' * b' ∈ closure (S * T)
    exact subset_closure (Set.mul_mem_mul ha' hb')
  · rw [closure_le]
    rintro _ ⟨a, ha, b, hb, rfl⟩
    exact mul_mem_mul (subset_closure ha) (subset_closure hb)

lemma mul_eq_closure_mul_set (M N : AddSubmonoid R) : M * N = closure (M * N : Set R) := by
  rw [← closure_mul_closure, closure_eq, closure_eq]

@[simp] lemma mul_bot (S : AddSubmonoid R) : S * ⊥ = ⊥ := addSubmonoid_smul_bot S

-- need `zero_smul` to generalize to `SMul`
@[simp]
lemma bot_mul (S : AddSubmonoid R) : ⊥ * S = ⊥ :=
  eq_bot_iff.2 <| mul_le.2 fun m hm n _ => by rw [AddSubmonoid.mem_bot] at hm ⊢; rw [hm, zero_mul]

variable {M N P Q : AddSubmonoid R}

@[mono, gcongr] lemma mul_le_mul (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q := smul_le_smul hmp hnq

lemma mul_le_mul_left (h : M ≤ N) : M * P ≤ N * P := smul_le_smul_left h
lemma mul_le_mul_right (h : N ≤ P) : M * N ≤ M * P := smul_le_smul_right h

lemma mul_subset_mul : (↑M : Set R) * (↑N : Set R) ⊆ (↑(M * N) : Set R) := smul_subset_smul

lemma mul_sup : M * (N ⊔ P) = M * N ⊔ M * P := addSubmonoid_smul_sup

-- need `zero_smul` and `add_smul` to generalize to `SMul`
lemma sup_mul : (M ⊔ N) * P = M * P ⊔ N * P :=
  le_antisymm (mul_le.mpr fun mn hmn p hp ↦ by
    obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn
    rw [right_distrib]; exact add_mem_sup (mul_mem_mul hm hp) <| mul_mem_mul hn hp)
    (sup_le (mul_le_mul_left le_sup_left) <| mul_le_mul_left le_sup_right)

variable {ι : Sort*}

-- need `zero_smul` and `add_smul` to generalize to `SMul`
lemma iSup_mul (S : ι → AddSubmonoid R) (T : AddSubmonoid R) : (⨆ i, S i) * T = ⨆ i, S i * T :=
  le_antisymm (mul_le.mpr fun s hs t ht ↦ iSup_induction _ (motive := (· * t ∈ _)) hs
      (fun i s hs ↦ mem_iSup_of_mem i <| mul_mem_mul hs ht) (by simp_rw [zero_mul]; apply zero_mem)
      fun _ _ ↦ by simp_rw [right_distrib]; apply add_mem) <|
    iSup_le fun i ↦ mul_le_mul_left (le_iSup _ i)

lemma mul_iSup (T : AddSubmonoid R) (S : ι → AddSubmonoid R) : (T * ⨆ i, S i) = ⨆ i, T * S i :=
  smul_iSup T S

lemma mul_comm_of_commute (h : ∀ m ∈ M, ∀ n ∈ N, Commute m n) : M * N = N * M :=
  le_antisymm (mul_le.mpr fun m hm n hn ↦ h m hm n hn ▸ mul_mem_mul hn hm)
    (mul_le.mpr fun n hn m hm ↦ h m hm n hn ▸ mul_mem_mul hm hn)

end NonUnitalNonAssocSemiring

section NonUnitalNonAssocRing
variable [NonUnitalNonAssocRing R]

/-- `AddSubmonoid.neg` distributes over multiplication.

This is available as an instance in the `Pointwise` locale. -/
protected def hasDistribNeg : HasDistribNeg (AddSubmonoid R) where
  neg_mul x y := by
    refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_) <;>
        simp only [AddSubmonoid.mem_neg, ← neg_mul] at *
    · exact mul_mem_mul hm hn
    · exact mul_mem_mul (neg_mem_neg.2 hm) hn
  mul_neg x y := by
    refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_) <;>
        simp only [AddSubmonoid.mem_neg, ← mul_neg] at *
    · exact mul_mem_mul hm hn
    · exact mul_mem_mul hm (neg_mem_neg.2 hn)

scoped[Pointwise] attribute [instance] AddSubmonoid.hasDistribNeg

end NonUnitalNonAssocRing

section NonAssocSemiring
variable [NonAssocSemiring R]

/-- A `MulOneClass` structure on additive submonoids of a (possibly, non-associative) semiring. -/
protected def mulOneClass : MulOneClass (AddSubmonoid R) where
  one_mul M := by rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, one_mul]
  mul_one M := by rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, mul_one]

scoped[Pointwise] attribute [instance] AddSubmonoid.mulOneClass

end NonAssocSemiring

section NonUnitalSemiring
variable [NonUnitalSemiring R]

/-- Semigroup structure on additive submonoids of a (possibly, non-unital) semiring. -/
protected def semigroup : Semigroup (AddSubmonoid R) where
  mul_assoc _M _N _P :=
    le_antisymm
      (mul_le.2 fun _mn hmn p hp => AddSubmonoid.mul_induction_on hmn
        (fun m hm n hn ↦ mul_assoc m n p ▸ mul_mem_mul hm <| mul_mem_mul hn hp)
        fun x y ↦ (add_mul x y p).symm ▸ add_mem)
      (mul_le.2 fun m hm _np hnp => AddSubmonoid.mul_induction_on hnp
        (fun n hn p hp ↦ mul_assoc m n p ▸ mul_mem_mul (mul_mem_mul hm hn) hp)
        fun x y ↦ (mul_add m x y) ▸ add_mem)

scoped[Pointwise] attribute [instance] AddSubmonoid.semigroup

end NonUnitalSemiring

section Semiring
variable [Semiring R]

/-- Monoid structure on additive submonoids of a semiring. -/
protected def monoid : Monoid (AddSubmonoid R) where

scoped[Pointwise] attribute [instance] AddSubmonoid.monoid

lemma closure_pow (s : Set R) : ∀ n : ℕ, closure s ^ n = closure (s ^ n)
  | 0 => by rw [pow_zero, pow_zero, one_eq_closure_one_set]
  | n + 1 => by rw [pow_succ, pow_succ, closure_pow s n, closure_mul_closure]

lemma pow_eq_closure_pow_set (s : AddSubmonoid R) (n : ℕ) :
    s ^ n = closure ((s : Set R) ^ n) := by
  rw [← closure_pow, closure_eq]

lemma pow_subset_pow {s : AddSubmonoid R} {n : ℕ} : (↑s : Set R) ^ n ⊆ ↑(s ^ n) :=
  (pow_eq_closure_pow_set s n).symm ▸ subset_closure

end Semiring
end AddSubmonoid
